\begin{figure}[!t]
	\centering
	\begin{lstlisting}
// 接口fopen的IMSpec实例，打开第一个参数指向的文件，如果失败则返回空指针
(*@\textcolor{blue}{Spec:}@*)
(*@\textcolor{blue}{Target:}@*) fopen(char*, char*) -> FILE*
(*@\textcolor{blue}{Pre:}@*) 
(*@\textcolor{black}{- fopen\_arg\_1 != NULL, }@*)
(*@\textcolor{black}{- fopen\_arg\_2 IN (r, w, a, r+, w+, a+)}@*)
(*@\textcolor{blue}{Post:}@*) 
// 异常检测以及异常处理操作
(*@\textcolor{black}{- fopen\_arg\_0 == NULL, RETURN(foo:FILEERR);}@*)
// 正确执行，需要关闭文件
(*@\textcolor{black}{- fopen\_arg\_0 != NULL, CALL(fclose: fopen\_arg\_0 == fclose\_arg\_1)}@*)

// 接口fgets的IMSpec实例，从第三个参数中读取第二个参数个字符到第一个参数中，
// 如果出错返回空指针
(*@\textcolor{blue}{Spec:}@*)
(*@\textcolor{blue}{Target:}@*) fgets(char*, int, FILE*) -> char*
(*@\textcolor{blue}{Pre:}@*) // omit single parameter validation
(*@\textcolor{black}{- LEN(fgets\_arg\_1) >= fgets\_arg\_2 }@*)
(*@\textcolor{blue}{Post:}@*)
// 异常检测以及异常处理操作 
(*@\textcolor{black}{- fgets\_arg\_0 == NULL, CALL(log: true), RETURN(\_:IOERR)}@*)
	\end{lstlisting}
	\caption{
		图~\ref{fig:2-4-example}中目标接口的IMSpec实例
	}
	\label{fig:2-4-example-imspec}
\end{figure}